Poster-child example courtesy of @hannes-steffenhagen-diffblue:

#include <assert.h>
#include <string.h>
#include <stdlib.h>


char *nondet_str(void) {
  const char empty[] = "                               ";
  char *result = strdup(empty);
  int x;
  __CPROVER_assume(x >= 0 && x <= 9);
  result[30] = (char)('0'+x);
  return result;
}

int main(void) {
  long x = 2;
  const char *sx = "                              2";
  for(int i = 0; i < 10; ++i) {
    assert(strtol(nondet_str(), NULL, 10) == x);
  }
  return 0;
}

This previously got bogged down in an ever-growing guard, I think because the guard |= operator didn't quite manage to squash the guard back down so that it left strtol in the same state as it entered, and so the run slowed ever down and down. With this patch that example takes around 5 seconds to complete on my machine.

Guards getting fat & monstrous has bugged me for many years -- and I believe it's a major performance problem.
I agree it's probably not sensible to try to solve this exactly, but that cheap, syntactic stuff is the way to go.
Other ideas like "function body"?

Another BTW: I think that path-pased symex suffers from this just as much.

@kroening I don't follow "function body"?

SVCOMP/Java: 3 tests stop timing out (timeout = 30 seconds), overall CPU time down 5%

SVCOMP/C subsample: 3 tests stop timing out (timeout = 30 seconds), total CPU time down 2%

CI failure: this harms performance for cases with many conditional ASSUME false; instructions in one function -- previously these would be ignored for guard purposes and the unviable instructions executed regardless, which was wasteful but lead to the guard being simplified more effectively. This is especially punitive with BDD guards.

Note this already happens now when paths are truncated by falsifying the guard -- for example exceeding depth bound, or the (specifically recursion) unwind bound.

Proposed course of action: merge this PR with the guard reversion but not the path truncation cleanup, then separately pursue guard shrinkage when paths are truncated, then make path truncation uniform so that we don't execute instructions after an ASSUME false.

In view of this I've removed the cleanup of ASSUME vs. guard manipulation from this PR and only make the on-function-return guard simplification. I'm re-running my benchmarks on this modified version and expect CI to pass here.

Current status: causes about 10 SVCOMP/Java tests to stop timing out and instead return incorrect answers. Looking into it...

Codecov Report

Merging #5003 into develop will decrease coverage by 0.04%.
The diff coverage is 100%.

@@             Coverage Diff             @@
##           develop    #5003      +/-   ##
===========================================
- Coverage    69.47%   69.43%   -0.05%     
===========================================
  Files         1310     1310              
  Lines       108763   108741      -22     
===========================================
- Hits         75566    75502      -64     
- Misses       33197    33239      +42

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update bb6baff...66133a6. Read the comment docs.

Conclusion: reintroduced those parts of the cleanup that ensure an ASSUME / real constraint is generated wherever we truncate execution due to the unwind or depth limits, as otherwise using the dominant guard would actually mean broadening the guard by re-including impossible paths. This PR now (a) ensures we generate a real constraint whenever we truncate a path, and (b) uses guard-as-of-entering-function whenever we exit that function, possibly broadening it by including paths that have been ruled out and/or simplifying it better than the expression-simplifier is capable of.

Forthcoming work will separate the concepts of guards and reachability, such that we can reduce the execution guard at control-flow convergances even when one of the predecessors is unreachable, while maintaining the benefit of not generating constraints for unreachable code.

Re-benchmarked with neutral results: all I claim now is that specific examples where the guard gets out of hand, like Hannes' example above, become analysable with this change but were previously impractically slow.